0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 601 ms)
↳10 BOUNDS(1, n^1)
a__and(true, X) → mark(X)
a__and(false, Y) → false
a__if(true, X, Y) → mark(X)
a__if(false, X, Y) → mark(Y)
a__add(0, X) → mark(X)
a__add(s(X), Y) → s(add(X, Y))
a__first(0, X) → nil
a__first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
a__from(X) → cons(X, from(s(X)))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(if(X1, X2, X3)) → a__if(mark(X1), X2, X3)
mark(add(X1, X2)) → a__add(mark(X1), X2)
mark(first(X1, X2)) → a__first(mark(X1), mark(X2))
mark(from(X)) → a__from(X)
mark(true) → true
mark(false) → false
mark(0) → 0
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__if(X1, X2, X3) → if(X1, X2, X3)
a__add(X1, X2) → add(X1, X2)
a__first(X1, X2) → first(X1, X2)
a__from(X) → from(X)
a__and(true, X) → mark(X) [1]
a__and(false, Y) → false [1]
a__if(true, X, Y) → mark(X) [1]
a__if(false, X, Y) → mark(Y) [1]
a__add(0, X) → mark(X) [1]
a__add(s(X), Y) → s(add(X, Y)) [1]
a__first(0, X) → nil [1]
a__first(s(X), cons(Y, Z)) → cons(Y, first(X, Z)) [1]
a__from(X) → cons(X, from(s(X))) [1]
mark(and(X1, X2)) → a__and(mark(X1), X2) [1]
mark(if(X1, X2, X3)) → a__if(mark(X1), X2, X3) [1]
mark(add(X1, X2)) → a__add(mark(X1), X2) [1]
mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) [1]
mark(from(X)) → a__from(X) [1]
mark(true) → true [1]
mark(false) → false [1]
mark(0) → 0 [1]
mark(s(X)) → s(X) [1]
mark(nil) → nil [1]
mark(cons(X1, X2)) → cons(X1, X2) [1]
a__and(X1, X2) → and(X1, X2) [1]
a__if(X1, X2, X3) → if(X1, X2, X3) [1]
a__add(X1, X2) → add(X1, X2) [1]
a__first(X1, X2) → first(X1, X2) [1]
a__from(X) → from(X) [1]
a__and(true, X) → mark(X) [1]
a__and(false, Y) → false [1]
a__if(true, X, Y) → mark(X) [1]
a__if(false, X, Y) → mark(Y) [1]
a__add(0, X) → mark(X) [1]
a__add(s(X), Y) → s(add(X, Y)) [1]
a__first(0, X) → nil [1]
a__first(s(X), cons(Y, Z)) → cons(Y, first(X, Z)) [1]
a__from(X) → cons(X, from(s(X))) [1]
mark(and(X1, X2)) → a__and(mark(X1), X2) [1]
mark(if(X1, X2, X3)) → a__if(mark(X1), X2, X3) [1]
mark(add(X1, X2)) → a__add(mark(X1), X2) [1]
mark(first(X1, X2)) → a__first(mark(X1), mark(X2)) [1]
mark(from(X)) → a__from(X) [1]
mark(true) → true [1]
mark(false) → false [1]
mark(0) → 0 [1]
mark(s(X)) → s(X) [1]
mark(nil) → nil [1]
mark(cons(X1, X2)) → cons(X1, X2) [1]
a__and(X1, X2) → and(X1, X2) [1]
a__if(X1, X2, X3) → if(X1, X2, X3) [1]
a__add(X1, X2) → add(X1, X2) [1]
a__first(X1, X2) → first(X1, X2) [1]
a__from(X) → from(X) [1]
| a__and :: true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if true :: true:false:0:s:add:nil:cons:first:from:and:if mark :: true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if false :: true:false:0:s:add:nil:cons:first:from:and:if a__if :: true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if a__add :: true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if 0 :: true:false:0:s:add:nil:cons:first:from:and:if s :: true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if add :: true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if a__first :: true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if nil :: true:false:0:s:add:nil:cons:first:from:and:if cons :: true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if first :: true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if a__from :: true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if from :: true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if and :: true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if if :: true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if → true:false:0:s:add:nil:cons:first:from:and:if |
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
true => 3
false => 1
0 => 0
nil => 2
a__add(z, z') -{ 1 }→ mark(X) :|: z' = X, X >= 0, z = 0
a__add(z, z') -{ 1 }→ 1 + (1 + X + Y) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0
a__add(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
a__and(z, z') -{ 1 }→ mark(X) :|: z' = X, z = 3, X >= 0
a__and(z, z') -{ 1 }→ 1 :|: z' = Y, Y >= 0, z = 1
a__and(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
a__first(z, z') -{ 1 }→ 2 :|: z' = X, X >= 0, z = 0
a__first(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
a__first(z, z') -{ 1 }→ 1 + Y + (1 + X + Z) :|: Z >= 0, z = 1 + X, Y >= 0, X >= 0, z' = 1 + Y + Z
a__from(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
a__from(z) -{ 1 }→ 1 + X + (1 + (1 + X)) :|: X >= 0, z = X
a__if(z, z', z'') -{ 1 }→ mark(X) :|: z' = X, z = 3, Y >= 0, z'' = Y, X >= 0
a__if(z, z', z'') -{ 1 }→ mark(Y) :|: z' = X, Y >= 0, z = 1, z'' = Y, X >= 0
a__if(z, z', z'') -{ 1 }→ 1 + X1 + X2 + X3 :|: X1 >= 0, X3 >= 0, X2 >= 0, z = X1, z' = X2, z'' = X3
mark(z) -{ 1 }→ a__if(mark(X1), X2, X3) :|: X1 >= 0, X3 >= 0, z = 1 + X1 + X2 + X3, X2 >= 0
mark(z) -{ 1 }→ a__from(X) :|: z = 1 + X, X >= 0
mark(z) -{ 1 }→ a__first(mark(X1), mark(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
mark(z) -{ 1 }→ a__and(mark(X1), X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
mark(z) -{ 1 }→ a__add(mark(X1), X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
mark(z) -{ 1 }→ 3 :|: z = 3
mark(z) -{ 1 }→ 2 :|: z = 2
mark(z) -{ 1 }→ 1 :|: z = 1
mark(z) -{ 1 }→ 0 :|: z = 0
mark(z) -{ 1 }→ 1 + X :|: z = 1 + X, X >= 0
mark(z) -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
| eq(start(V, V1, V2),0,[fun(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2),0,[fun1(V, V1, V2, Out)],[V >= 0,V1 >= 0,V2 >= 0]). eq(start(V, V1, V2),0,[fun2(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2),0,[fun3(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2),0,[fun4(V, Out)],[V >= 0]). eq(start(V, V1, V2),0,[mark(V, Out)],[V >= 0]). eq(fun(V, V1, Out),1,[mark(X4, Ret)],[Out = Ret,V1 = X4,V = 3,X4 >= 0]). eq(fun(V, V1, Out),1,[],[Out = 1,V1 = Y1,Y1 >= 0,V = 1]). eq(fun1(V, V1, V2, Out),1,[mark(X5, Ret1)],[Out = Ret1,V1 = X5,V = 3,Y2 >= 0,V2 = Y2,X5 >= 0]). eq(fun1(V, V1, V2, Out),1,[mark(Y3, Ret2)],[Out = Ret2,V1 = X6,Y3 >= 0,V = 1,V2 = Y3,X6 >= 0]). eq(fun2(V, V1, Out),1,[mark(X7, Ret3)],[Out = Ret3,V1 = X7,X7 >= 0,V = 0]). eq(fun2(V, V1, Out),1,[],[Out = 2 + X8 + Y4,V = 1 + X8,V1 = Y4,Y4 >= 0,X8 >= 0]). eq(fun3(V, V1, Out),1,[],[Out = 2,V1 = X9,X9 >= 0,V = 0]). eq(fun3(V, V1, Out),1,[],[Out = 2 + X10 + Y5 + Z1,Z1 >= 0,V = 1 + X10,Y5 >= 0,X10 >= 0,V1 = 1 + Y5 + Z1]). eq(fun4(V, Out),1,[],[Out = 3 + 2*X11,X11 >= 0,V = X11]). eq(mark(V, Out),1,[mark(X12, Ret0),fun(Ret0, X21, Ret4)],[Out = Ret4,X12 >= 0,X21 >= 0,V = 1 + X12 + X21]). eq(mark(V, Out),1,[mark(X13, Ret01),fun1(Ret01, X22, X31, Ret5)],[Out = Ret5,X13 >= 0,X31 >= 0,V = 1 + X13 + X22 + X31,X22 >= 0]). eq(mark(V, Out),1,[mark(X14, Ret02),fun2(Ret02, X23, Ret6)],[Out = Ret6,X14 >= 0,X23 >= 0,V = 1 + X14 + X23]). eq(mark(V, Out),1,[mark(X15, Ret03),mark(X24, Ret11),fun3(Ret03, Ret11, Ret7)],[Out = Ret7,X15 >= 0,X24 >= 0,V = 1 + X15 + X24]). eq(mark(V, Out),1,[fun4(X16, Ret8)],[Out = Ret8,V = 1 + X16,X16 >= 0]). eq(mark(V, Out),1,[],[Out = 3,V = 3]). eq(mark(V, Out),1,[],[Out = 1,V = 1]). eq(mark(V, Out),1,[],[Out = 0,V = 0]). eq(mark(V, Out),1,[],[Out = 1 + X17,V = 1 + X17,X17 >= 0]). eq(mark(V, Out),1,[],[Out = 2,V = 2]). eq(mark(V, Out),1,[],[Out = 1 + X18 + X25,X18 >= 0,X25 >= 0,V = 1 + X18 + X25]). eq(fun(V, V1, Out),1,[],[Out = 1 + X19 + X26,X19 >= 0,X26 >= 0,V = X19,V1 = X26]). eq(fun1(V, V1, V2, Out),1,[],[Out = 1 + X110 + X27 + X32,X110 >= 0,X32 >= 0,X27 >= 0,V = X110,V1 = X27,V2 = X32]). eq(fun2(V, V1, Out),1,[],[Out = 1 + X111 + X28,X111 >= 0,X28 >= 0,V = X111,V1 = X28]). eq(fun3(V, V1, Out),1,[],[Out = 1 + X112 + X29,X112 >= 0,X29 >= 0,V = X112,V1 = X29]). eq(fun4(V, Out),1,[],[Out = 1 + X20,X20 >= 0,V = X20]). input_output_vars(fun(V,V1,Out),[V,V1],[Out]). input_output_vars(fun1(V,V1,V2,Out),[V,V1,V2],[Out]). input_output_vars(fun2(V,V1,Out),[V,V1],[Out]). input_output_vars(fun3(V,V1,Out),[V,V1],[Out]). input_output_vars(fun4(V,Out),[V],[Out]). input_output_vars(mark(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [fun3/3]
1. non_recursive : [fun4/2]
2. recursive [non_tail,multiple] : [fun/3,fun1/4,fun2/3,mark/2]
3. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into fun3/3
1. SCC is partially evaluated into fun4/2
2. SCC is partially evaluated into mark/2
3. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations fun3/3
* CE 20 is refined into CE [24]
* CE 21 is refined into CE [25]
* CE 19 is refined into CE [26]
### Cost equations --> "Loop" of fun3/3
* CEs [24] --> Loop 16
* CEs [25] --> Loop 17
* CEs [26] --> Loop 18
### Ranking functions of CR fun3(V,V1,Out)
#### Partial ranking functions of CR fun3(V,V1,Out)
### Specialization of cost equations fun4/2
* CE 22 is refined into CE [27]
* CE 23 is refined into CE [28]
### Cost equations --> "Loop" of fun4/2
* CEs [27] --> Loop 19
* CEs [28] --> Loop 20
### Ranking functions of CR fun4(V,Out)
#### Partial ranking functions of CR fun4(V,Out)
### Specialization of cost equations mark/2
* CE 15 is refined into CE [29,30]
* CE 16 is refined into CE [31]
* CE 17 is refined into CE [32]
* CE 18 is refined into CE [33]
* CE 12 is refined into CE [34]
* CE 11 is refined into CE [35]
* CE 10 is refined into CE [36]
* CE 14 is refined into CE [37,38,39]
* CE 9 is refined into CE [40]
* CE 13 is refined into CE [41]
### Cost equations --> "Loop" of mark/2
* CEs [40] --> Loop 21
* CEs [41] --> Loop 22
* CEs [39] --> Loop 23
* CEs [38] --> Loop 24
* CEs [34] --> Loop 25
* CEs [35] --> Loop 26
* CEs [36] --> Loop 27
* CEs [37] --> Loop 28
* CEs [30] --> Loop 29
* CEs [29,31,32] --> Loop 30
* CEs [33] --> Loop 31
### Ranking functions of CR mark(V,Out)
* RF of phase [21,22,23,24,25,26,27,28]: [V]
#### Partial ranking functions of CR mark(V,Out)
* Partial RF of phase [21,22,23,24,25,26,27,28]:
- RF of loop [21:1,22:1,23:1,23:2,24:1,24:2,25:1,25:2,26:1,26:2,27:1,27:2,28:1,28:2]:
V
### Specialization of cost equations start/3
* CE 5 is refined into CE [42,43,44]
* CE 4 is refined into CE [45,46,47]
* CE 2 is refined into CE [48]
* CE 3 is refined into CE [49,50,51]
* CE 6 is refined into CE [52,53,54]
* CE 7 is refined into CE [55,56]
* CE 8 is refined into CE [57,58,59]
### Cost equations --> "Loop" of start/3
* CEs [43,44] --> Loop 32
* CEs [42] --> Loop 33
* CEs [46,47] --> Loop 34
* CEs [45] --> Loop 35
* CEs [48,49,50,51,52,53,54,55,56,57,58,59] --> Loop 36
### Ranking functions of CR start(V,V1,V2)
#### Partial ranking functions of CR start(V,V1,V2)
Computing Bounds
=====================================
#### Cost of chains of fun3(V,V1,Out):
* Chain [18]: 1
with precondition: [V=0,Out=2,V1>=0]
* Chain [17]: 1
with precondition: [V+V1+1=Out,V>=0,V1>=0]
* Chain [16]: 1
with precondition: [V+V1=Out,V>=1,V1>=1]
#### Cost of chains of fun4(V,Out):
* Chain [20]: 1
with precondition: [V+1=Out,V>=0]
* Chain [19]: 1
with precondition: [2*V+3=Out,V>=0]
#### Cost of chains of mark(V,Out):
* Chain [31]: 1
with precondition: [V=0,Out=0]
* Chain [30]: 2
with precondition: [V=Out,V>=1]
* Chain [29]: 2
with precondition: [2*V+1=Out,V>=1]
* Chain [multiple([21,22,23,24,25,26,27,28],[[31],[30],[29]])]: 4*it(21)+2*it(23)+6*it(24)+2*it(25)+2*it(26)+4*it([29])+1*it([31])+0
Such that:aux(10) =< 1
aux(11) =< V
aux(12) =< 2/3*V
aux(13) =< 4/3*V+1/3
aux(14) =< 6/7*V
it(21) =< aux(11)
it(23) =< aux(11)
it(24) =< aux(11)
it(25) =< aux(11)
it(26) =< aux(11)
it([29]) =< aux(11)
it(25) =< aux(12)
it(24) =< aux(13)
it(25) =< aux(13)
it(26) =< aux(13)
it([29]) =< aux(13)
it(23) =< aux(14)
it(25) =< aux(14)
it(26) =< aux(14)
it([29]) =< it(24)+it(24)+it(26)+it(25)+it(24)+it(23)+aux(10)
it([31]) =< it(24)+it(24)+it(26)+it(25)+it(24)+it(23)+aux(10)
with precondition: [V>=1,Out>=0,5*V>=2*Out+1,2*V+1>=Out]
#### Cost of chains of start(V,V1,V2):
* Chain [36]: 4*s(18)+2*s(19)+6*s(20)+2*s(21)+2*s(22)+4*s(23)+1*s(24)+4*s(30)+2*s(31)+6*s(32)+2*s(33)+2*s(34)+4*s(35)+1*s(36)+3
Such that:s(26) =< V
s(27) =< 2/3*V
s(28) =< 4/3*V+1/3
s(29) =< 6/7*V
s(14) =< V1
s(15) =< 2/3*V1
s(16) =< 4/3*V1+1/3
s(17) =< 6/7*V1
aux(15) =< 1
s(18) =< s(14)
s(19) =< s(14)
s(20) =< s(14)
s(21) =< s(14)
s(22) =< s(14)
s(23) =< s(14)
s(21) =< s(15)
s(20) =< s(16)
s(21) =< s(16)
s(22) =< s(16)
s(23) =< s(16)
s(19) =< s(17)
s(21) =< s(17)
s(22) =< s(17)
s(23) =< s(20)+s(20)+s(22)+s(21)+s(20)+s(19)+aux(15)
s(24) =< s(20)+s(20)+s(22)+s(21)+s(20)+s(19)+aux(15)
s(30) =< s(26)
s(31) =< s(26)
s(32) =< s(26)
s(33) =< s(26)
s(34) =< s(26)
s(35) =< s(26)
s(33) =< s(27)
s(32) =< s(28)
s(33) =< s(28)
s(34) =< s(28)
s(35) =< s(28)
s(31) =< s(29)
s(33) =< s(29)
s(34) =< s(29)
s(35) =< s(32)+s(32)+s(34)+s(33)+s(32)+s(31)+aux(15)
s(36) =< s(32)+s(32)+s(34)+s(33)+s(32)+s(31)+aux(15)
with precondition: [V>=0]
* Chain [35]: 2
with precondition: [V=1,V2=0,V1>=0]
* Chain [34]: 4*s(42)+2*s(43)+6*s(44)+2*s(45)+2*s(46)+4*s(47)+1*s(48)+3
Such that:s(37) =< 1
s(38) =< V2
s(39) =< 2/3*V2
s(40) =< 4/3*V2+1/3
s(41) =< 6/7*V2
s(42) =< s(38)
s(43) =< s(38)
s(44) =< s(38)
s(45) =< s(38)
s(46) =< s(38)
s(47) =< s(38)
s(45) =< s(39)
s(44) =< s(40)
s(45) =< s(40)
s(46) =< s(40)
s(47) =< s(40)
s(43) =< s(41)
s(45) =< s(41)
s(46) =< s(41)
s(47) =< s(44)+s(44)+s(46)+s(45)+s(44)+s(43)+s(37)
s(48) =< s(44)+s(44)+s(46)+s(45)+s(44)+s(43)+s(37)
with precondition: [V=1,V1>=0,V2>=1]
* Chain [33]: 2
with precondition: [V=3,V1=0]
* Chain [32]: 4*s(54)+2*s(55)+6*s(56)+2*s(57)+2*s(58)+4*s(59)+1*s(60)+3
Such that:s(49) =< 1
s(50) =< V1
s(51) =< 2/3*V1
s(52) =< 4/3*V1+1/3
s(53) =< 6/7*V1
s(54) =< s(50)
s(55) =< s(50)
s(56) =< s(50)
s(57) =< s(50)
s(58) =< s(50)
s(59) =< s(50)
s(57) =< s(51)
s(56) =< s(52)
s(57) =< s(52)
s(58) =< s(52)
s(59) =< s(52)
s(55) =< s(53)
s(57) =< s(53)
s(58) =< s(53)
s(59) =< s(56)+s(56)+s(58)+s(57)+s(56)+s(55)+s(49)
s(60) =< s(56)+s(56)+s(58)+s(57)+s(56)+s(55)+s(49)
with precondition: [V=3,V1>=1]
Closed-form bounds of start(V,V1,V2):
-------------------------------------
* Chain [36] with precondition: [V>=0]
- Upper bound: 26*V+5+nat(V1)*26
- Complexity: n
* Chain [35] with precondition: [V=1,V2=0,V1>=0]
- Upper bound: 2
- Complexity: constant
* Chain [34] with precondition: [V=1,V1>=0,V2>=1]
- Upper bound: 26*V2+4
- Complexity: n
* Chain [33] with precondition: [V=3,V1=0]
- Upper bound: 2
- Complexity: constant
* Chain [32] with precondition: [V=3,V1>=1]
- Upper bound: 26*V1+4
- Complexity: n
### Maximum cost of start(V,V1,V2): max([nat(V2)*26+2,nat(V1)*26+2+ (26*V+1)])+2
Asymptotic class: n
* Total analysis performed in 444 ms.